Nuprl Lemma : assert-fpf-is-empty 0,22

A:Type, B:(AType), f:x:A fp B(x). fpf-is-empty(f f =  
latex


Definitions2of(t), 1of(t), True, False, , Unit, x:AB(x), A & B, , AB, A, P  Q, P & Q, P  Q, P  Q, , Prop, xt(x), a:A fp B(a), , fpf-is-empty(f), x(s), (x  l), i=j, ||as||, x:AB(x), t  T, b
Lemmaslength wf1, eq int wf, fpf wf, fpf-empty wf, assert wf, l member wf, length zero, assert of eq int, false wf, unit wf, it wf, pi1 wf, pi2 wf

origin